diff options
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 9515c5de9..d11454b27 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -536,10 +536,10 @@ struct let get_left_construct term = match Term.kind_of_term term with - | Term.Construct(_,i) -> (i,[| |]) + | Term.Construct((_,i),_) -> (i,[| |]) | Term.App(l,rst) -> (match Term.kind_of_term l with - | Term.Construct(_,i) -> (i,rst) + | Term.Construct((_,i),_) -> (i,rst) | _ -> raise ParseError ) | _ -> raise ParseError @@ -833,8 +833,8 @@ struct let parse_zop (op,args) = match kind_of_term op with - | Const x -> (assoc_const op zop_table, args.(0) , args.(1)) - | Ind(n,0) -> + | Const (x,_) -> (assoc_const op zop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_Z) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -842,8 +842,8 @@ struct let parse_rop (op,args) = match kind_of_term op with - | Const x -> (assoc_const op rop_table, args.(0) , args.(1)) - | Ind(n,0) -> + | Const (x,_) -> (assoc_const op rop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_R) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError |