diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-07 20:27:24 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-07 20:27:24 +0000 |
| commit | c63367d05354834211cadb38340334960e8106f8 (patch) | |
| tree | 29af35131d7857fc860c1ef381c3e5f6d4dfaa21 /toplevel | |
| parent | a20115809c0c6a36124366fae64130e3e513c1f1 (diff) | |
Fix implicit arguments in sections bug and check for resolution of evars when
defining records. Fix test-suite script because of new implicit argument
setting for DefaultRelation. Fix regression in auto, changing the order
of tried lemmas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11213 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/record.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index ab06673e4..5a9e014d4 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -65,6 +65,11 @@ let typecheck_params_and_fields id t ps fs = let env2,impls,newfs,data = interp_fields_evars evars env_ar (binders_of_decls fs) in + let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in + let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in + let ce t = Evarutil.check_evars env0 Evd.empty !evars t in + List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps; + List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs; imps, newps, impls, newfs let degenerate_decl (na,b,t) = |