mattam82/coq

Anomaly Not Found with Implicit arguments (IR)

amblafont opened this issue · 1 comments

amblafont commented 
Set Implicit Arguments.

Inductive bete :  Type :=
| Cbete  : forall mtt e, @rec mtt e  -> bete  
  fix rec (mtt :unit) (e: mtt = tt ) :Type  := unit.

This raises an anomaly (uncaught exception Not_found) which disappears if 'Set Implicit Arguments' is removed

mattam82 commented

Fixed now, explicit implicits with {foo: T} work as well now.