diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:03 +0000 |
| commit | 4a39b5cb9841a9e11b745bce0d3dc2bc86d6b185 (patch) | |
| tree | ab90f9acc3dc2038ea17367afb2cc4285a77f1b2 /plugins/funind/merge.ml | |
| parent | a3ab8b07b912afd1b883ed60bd532b5a29bccd8f (diff) | |
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15382 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 4ca23a295..ebe5cebd2 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -830,7 +830,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = glob_constr_to_constr_expr tp in - LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc) + LocalRawAssum ([(dummy_loc,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) concl in let arity,_ = @@ -838,7 +838,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = (fun (acc,env) (nm,_,c) -> let typ = Constrextern.extern_constr false env c in let newenv = Environ.push_rel (nm,None,c) env in - CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv) + CProdN (dummy_loc, [[(dummy_loc,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in |