aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/clenv.ml91
-rw-r--r--pretyping/clenv.mli8
-rw-r--r--pretyping/evd.ml6
-rw-r--r--pretyping/evd.mli2
-rw-r--r--pretyping/reductionops.ml19
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/clenvtac.ml27
-rw-r--r--tactics/auto.ml6
-rw-r--r--tactics/class_tactics.ml421
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/setoid_replace.ml2
-rw-r--r--tactics/tactics.ml6
-rw-r--r--test-suite/success/apply.v19
14 files changed, 70 insertions, 142 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index c5c246877..732ff1e69 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -54,77 +54,11 @@ let subst_clenv sub clenv =
env = clenv.env }
let clenv_nf_meta clenv c = nf_meta clenv.evd c
-let clenv_direct_nf_meta clenv c = direct_nf_meta clenv.evd c
let clenv_term clenv c = meta_instance clenv.evd c
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
let clenv_value clenv = meta_instance clenv.evd clenv.templval
-let clenv_direct_value clenv = nf_betaiota clenv.templval.rebus
let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
-let clenv_direct_nf_type clenv = nf_betaiota clenv.templtyp.rebus
-
-let plain_instance find c =
- let rec irec u = match kind_of_term u with
- | Meta p -> find p
- | App (f,l) when isCast f ->
- let (f,_,t) = destCast f in
- let l' = Array.map irec l in
- (match kind_of_term f with
- | Meta p ->
- (* Don't flatten application nodes: this is used to extract a
- proof-term from a proof-tree and we want to keep the structure
- of the proof-tree *)
- let g = find p in
- (match kind_of_term g with
- | App _ ->
- let h = id_of_string "H" in
- mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
- | _ -> mkApp (g,l'))
- | _ -> mkApp (irec f,l'))
- | Cast (m,_,_) when isMeta m -> find (destMeta m)
- | _ -> map_constr irec u
- in
- local_strong whd_betaiota
- (if c.freemetas = Metaset.empty then c.rebus else irec c.rebus)
-
-let clenv_expand_metas clenv =
- let seen = ref Metamap.empty in
- let ongoing = ref Metaset.empty in
- let todo = ref (meta_list clenv.evd) in
-
- let rec process_all () = match !todo with
- | [] -> ()
- | (mv,cl)::_ -> let _ = process_meta mv cl in process_all ()
-
- and process_meta mv cl =
- ongoing := Metaset.add mv !ongoing;
- let (body,typ) = match cl with
- | Clval (na,(body,status),typ) ->
- let body = plain_instance instance_of_meta body in
- let typ = plain_instance instance_of_meta typ in
- (body,Clval(na,(mk_freelisted body,status),mk_freelisted typ))
- | Cltyp (na,typ) ->
- let typ = plain_instance instance_of_meta typ in
- (mkMeta mv,Cltyp(na,mk_freelisted typ)) in
- ongoing := Metaset.remove mv !ongoing;
- seen := Metamap.add mv (body,typ) !seen;
- todo := List.remove_assoc mv !todo;
- body
-
- and instance_of_meta mv =
- try fst (Metamap.find mv !seen)
- with Not_found ->
- if Metaset.mem mv !ongoing then
- error "Cannot instantiate an existential variable with a term which depends on itself";
- process_meta mv (find_meta clenv.evd mv) in
-
- process_all ();
-
- { clenv with
- evd = replace_metas (Metamap.map snd !seen) clenv.evd;
- templtyp = mk_freelisted(plain_instance instance_of_meta clenv.templtyp);
- templval = mk_freelisted(plain_instance instance_of_meta clenv.templval)}
-
-let instantiated_clenv_template clenv = (clenv.templval,clenv.templtyp)
+
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
@@ -134,8 +68,7 @@ let clenv_get_type_of ce c =
exception NotExtensibleClause
let clenv_push_prod cl =
- let typ =
- whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_direct_nf_type cl) in
+ let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
let rec clrec typ = match kind_of_term typ with
| Cast (t,_,_) -> clrec t
| Prod (na,t,u) ->
@@ -280,9 +213,13 @@ let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
* returns a list of the metavars which appear in the type of
* the metavar mv. The list is unordered. *)
+let clenv_metavars evd mv =
+ (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+
let dependent_metas clenv mvs conclmetas =
List.fold_right
- (fun mv deps -> Metaset.union deps (meta_ftype clenv.evd mv).freemetas)
+ (fun mv deps ->
+ Metaset.union deps (clenv_metavars clenv.evd mv))
mvs conclmetas
let duplicated_metas c =
@@ -294,14 +231,14 @@ let duplicated_metas c =
snd (collrec ([],[]) c)
let clenv_dependent hyps_only clenv =
- let (body,typ) = instantiated_clenv_template clenv in
let mvs = undefined_metas clenv.evd in
- let deps = dependent_metas clenv mvs typ.freemetas in
- let nonlinear = duplicated_metas body.rebus in
+ let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
+ let deps = dependent_metas clenv mvs ctyp_mvs in
+ let nonlinear = duplicated_metas (clenv_value clenv) in
(* Make the assumption that duplicated metas have internal dependencies *)
List.filter
(fun mv -> (Metaset.mem mv deps &&
- not (hyps_only && Metaset.mem mv typ.freemetas))
+ not (hyps_only && Metaset.mem mv ctyp_mvs))
or List.mem mv nonlinear)
mvs
@@ -430,9 +367,9 @@ type arg_bindings = open_constr explicit_bindings
* of cval, ctyp. *)
let clenv_independent clenv =
- let (body,typ) = instantiated_clenv_template clenv in
- let mvs = Metaset.elements body.freemetas in
- let deps = dependent_metas clenv mvs typ.freemetas in
+ let mvs = collect_metas (clenv_value clenv) in
+ let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
+ let deps = dependent_metas clenv mvs ctyp_mvs in
List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
let check_bindings bl =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index de5a1e375..dfa751349 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -43,16 +43,10 @@ val subst_clenv : substitution -> clausenv -> clausenv
(* subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
-(* subject of clenv (assume it is pre-instantiated) *)
-val clenv_direct_value : clausenv -> constr
(* type of clenv (instantiated) *)
val clenv_type : clausenv -> types
-(* type of clenv (assume it is pre-instantiated) *)
-val clenv_direct_nf_type : clausenv -> types
(* substitute resolved metas *)
val clenv_nf_meta : clausenv -> constr -> constr
-(* substitute resolved metas (assume the metas in clausenv are expanded) *)
-val clenv_direct_nf_meta : clausenv -> constr -> constr
(* type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
@@ -89,8 +83,6 @@ val clenv_dependent : bool -> clausenv -> metavariable list
val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
-val clenv_expand_metas : clausenv -> clausenv
-
(***************************************************************)
(* Bindings *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2b9a0ed82..b29afc0cb 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -610,18 +610,12 @@ let meta_with_name evd id =
(str "Binder name \"" ++ pr_id id ++
strbrk "\" occurs more than once in clause.")
-let mk_meta_subst evd =
- Metamap.fold (fun mv cl subst -> match cl with
- | Clval(_,(b,_),typ) -> (mv, b.rebus) :: subst
- | Cltyp (_,typ) -> subst) evd.metas []
let meta_merge evd1 evd2 =
{evd2 with
metas = List.fold_left (fun m (n,v) -> Metamap.add n v m)
evd2.metas (metamap_to_list evd1.metas) }
-let replace_metas metas evd = { evd with metas = metas }
-
type metabinding = metavariable * constr * instance_status
let retract_coercible_metas evd =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 2fd668043..825096acc 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -218,7 +218,6 @@ val meta_declare :
metavariable -> types -> ?name:name -> evar_defs -> evar_defs
val meta_assign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
-val mk_meta_subst : evar_defs -> meta_value_map
(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
val meta_merge : evar_defs -> evar_defs -> evar_defs
@@ -226,7 +225,6 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs
val undefined_metas : evar_defs -> metavariable list
val metas_of : evar_defs -> meta_type_map
val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs
-val replace_metas : clbinding Metamap.t -> evar_defs -> evar_defs
type metabinding = metavariable * constr * instance_status
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7fdcded00..e24cf62bb 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -887,19 +887,28 @@ let meta_value evd mv =
in
valrec mv
-let meta_instance evd b =
+let meta_instance env b =
let c_sigma =
List.map
- (fun mv -> (mv,meta_value evd mv)) (Metaset.elements b.freemetas)
+ (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
in
if c_sigma = [] then b.rebus else instance c_sigma b.rebus
-let nf_meta evd c = meta_instance evd (mk_freelisted c)
-
-let direct_nf_meta evd c = instance (mk_meta_subst evd) c
+let nf_meta env c = meta_instance env (mk_freelisted c)
(* Instantiate metas that create beta/iota redexes *)
+let meta_value evd mv =
+ let rec valrec mv =
+ match meta_opt_fvalue evd mv with
+ | Some (b,_) ->
+ instance
+ (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
+ b.rebus
+ | None -> mkMeta mv
+ in
+ valrec mv
+
let meta_reducible_instance evd b =
let fm = Metaset.elements b.freemetas in
let metas = List.fold_left (fun l mv ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 397377473..371a66a9d 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -223,5 +223,4 @@ val whd_betaiota_deltazeta_for_iota_state : state_reduction_function
(*s Meta-related reduction functions *)
val meta_instance : evar_defs -> constr freelisted -> constr
val nf_meta : evar_defs -> constr -> constr
-val direct_nf_meta : evar_defs -> constr -> constr
val meta_reducible_instance : evar_defs -> constr freelisted -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a18db9026..a2671b5d1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -467,7 +467,7 @@ let unify_to_type env evd flags c u =
let sigma = evars_of evd in
let c = refresh_universes c in
let t = get_type_of_with_meta env sigma (metas_of evd) c in
- let t = Tacred.hnf_constr env sigma (nf_meta evd t) in
+ let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
let u = Tacred.hnf_constr env sigma u in
try unify_0 env sigma Cumul flags t u
with e when precatchable_exception e -> ([],[])
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index b1dc7c896..50529d32a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -40,31 +40,29 @@ open Clenv
let clenv_cast_meta clenv =
let rec crec u =
- match kind_of_term2 u with
+ match kind_of_term u with
| App _ | Case _ -> crec_hd u
- | Cast (Meta mv,_,_) | Meta mv ->
- (match Evd.meta_opt_fvalue clenv.evd mv with
- | Some (c,_) -> c.rebus
- | None -> u)
+ | Cast (c,_,_) when isMeta c -> u
| _ -> map_constr crec u
and crec_hd u =
match kind_of_term (strip_outer_cast u) with
| Meta mv ->
- (match Evd.find_meta clenv.evd mv with
- | Clval (_,(body,_),_) -> body.rebus
- | Cltyp (_,typ) ->
- if occur_meta typ.rebus then
- raise (RefinerError (MetaInType typ.rebus));
- mkCast (mkMeta mv, DEFAULTcast, typ.rebus))
+ (try
+ let b = Typing.meta_type clenv.evd mv in
+ assert (not (occur_meta b));
+ if occur_meta b then u
+ else mkCast (mkMeta mv, DEFAULTcast, b)
+ with Not_found -> u)
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
- | Case(ci,p,c,br) -> mkCase (ci, crec p, crec_hd c, Array.map crec br)
+ | Case(ci,p,c,br) ->
+ mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
| _ -> u
in
crec
let clenv_value_cast_meta clenv =
- clenv_cast_meta clenv (clenv_direct_value clenv)
+ clenv_cast_meta clenv (clenv_value clenv)
let clenv_pose_dependent_evars with_evars clenv =
let dep_mvs = clenv_dependent false clenv in
@@ -75,14 +73,13 @@ let clenv_pose_dependent_evars with_evars clenv =
let clenv_refine with_evars clenv gls =
- let clenv = clenv_expand_metas clenv in
let clenv = clenv_pose_dependent_evars with_evars clenv in
let evd' = Typeclasses.resolve_typeclasses ~fail:(not with_evars)
clenv.env clenv.evd
in
tclTHEN
(tclEVARS (evars_of evd'))
- (refine (clenv_value_cast_meta clenv))
+ (refine (clenv_cast_meta clenv (clenv_value clenv)))
gls
let dft = Unification.default_unify_flags
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 42d74f9ed..aa7ce1290 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -264,7 +264,7 @@ let make_exact_entry pri (c,cty) =
failwith "make_exact_entry"
| _ ->
let ce = mk_clenv_from dummy_goal (c,cty) in
- let c' = clenv_direct_nf_type ce in
+ let c' = clenv_type ce in
let pat = Pattern.pattern_of_constr c' in
(Some (head_of_constr_reference (List.hd (head_constr cty))),
{ pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
@@ -274,7 +274,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
match kind_of_term cty with
| Prod _ ->
let ce = mk_clenv_from dummy_goal (c,cty) in
- let c' = clenv_direct_nf_type ce in
+ let c' = clenv_type ce in
let pat = Pattern.pattern_of_constr c' in
let hd = (try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry") in
@@ -342,7 +342,7 @@ let make_trivial env sigma c =
let hd = head_of_constr_reference (List.hd (head_constr t)) in
let ce = mk_clenv_from dummy_goal (c,t) in
(Some hd, { pri=1;
- pat = Some (Pattern.pattern_of_constr (clenv_direct_nf_type ce));
+ pat = Some (Pattern.pattern_of_constr (clenv_type ce));
code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
open Vernacexpr
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 1ae1196a3..bda1fabbc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -751,7 +751,7 @@ let evd_convertible env evd x y =
let decompose_setoid_eqhyp env sigma c left2right =
let ctype = Typing.type_of env sigma c in
let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ctype) in
- let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
@@ -764,7 +764,7 @@ let decompose_setoid_eqhyp env sigma c left2right =
if not (evd_convertible env eqclause.evd ty1 ty2) then
error "The term does not end with an applied homogeneous relation."
else
- { cl=eqclause; prf=(Clenv.clenv_direct_value eqclause);
+ { cl=eqclause; prf=(Clenv.clenv_value eqclause);
car=ty1; rel=mkApp (equiv, Array.of_list others);
l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
@@ -808,7 +808,6 @@ let unify_eqn env sigma hypinfo t =
cl, prf, c1, c2, car, rel
else raise Not_found*)
let env' = clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in
- let env' = clenv_expand_metas env' in
let env' =
let mvs = clenv_dependent false env' in
clenv_pose_metas_as_evars env' mvs
@@ -819,8 +818,7 @@ let unify_eqn env sigma hypinfo t =
and rel = Clenv.clenv_nf_meta env' rel in
hypinfo := { !hypinfo with
cl = env';
- abs = Some (Clenv.clenv_direct_value env',
- Clenv.clenv_direct_nf_type env') };
+ abs = Some (Clenv.clenv_value env', Clenv.clenv_type env') };
env', prf, c1, c2, car, rel
| None ->
let env' =
@@ -831,7 +829,6 @@ let unify_eqn env sigma hypinfo t =
clenv_unify allowK ~flags:rewrite2_unif_flags
CONV left t cl
in
- let env' = clenv_expand_metas env' in
let env' =
let mvs = clenv_dependent false env' in
clenv_pose_metas_as_evars env' mvs
@@ -841,7 +838,7 @@ let unify_eqn env sigma hypinfo t =
let nf c = Evarutil.nf_evar (Evd.evars_of evd') (Clenv.clenv_nf_meta env' c) in
let c1 = nf c1 and c2 = nf c2
and car = nf car and rel = nf rel
- and prf = nf (Clenv.clenv_direct_value env') in
+ and prf = nf (Clenv.clenv_value env') in
let ty1 = Typing.mtype_of env'.env env'.evd c1
and ty2 = Typing.mtype_of env'.env env'.evd c2
in
@@ -1577,12 +1574,12 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
Unification.w_unify_to_subterm ~flags:rewrite2_unif_flags
(pf_env gl) ((if l2r then c1 else c2),but) cl.evd
in
- let cl' = clenv_expand_metas {cl with evd = env'} in
- let c1 = Clenv.clenv_direct_nf_meta cl' c1
- and c2 = Clenv.clenv_direct_nf_meta cl' c2 in
+ let cl' = {cl with evd = env'} in
+ let c1 = Clenv.clenv_nf_meta cl' c1
+ and c2 = Clenv.clenv_nf_meta cl' c2 in
check_evar_map_of_evars_defs env';
- let prf = Clenv.clenv_direct_value cl' in
- let prfty = Clenv.clenv_direct_nf_type cl' in
+ let prf = Clenv.clenv_value cl' in
+ let prfty = Clenv.clenv_type cl' in
let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
{cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 123c83e40..9994bd784 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -565,7 +565,7 @@ let apply_on_clause (f,t) clause =
(match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
| Meta mv -> mv
| _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
- clenv_expand_metas (clenv_fchain argmv f_clause clause)
+ clenv_fchain argmv f_clause clause
let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
let e = next_ident_away eq_baseid (ids_of_context env) in
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 22596ac3c..644a68666 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1815,7 +1815,7 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
let analyse_hypothesis gl c =
let ctype = pf_type_of gl c in
let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
- let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index be15311b9..87ef65d7c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -560,12 +560,11 @@ let error_uninstantiated_metas t clenv =
in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
let clenv_refine_in with_evars id clenv gl =
- let clenv = clenv_expand_metas clenv in
let clenv = clenv_pose_dependent_evars with_evars clenv in
let new_hyp_typ = clenv_type clenv in
if not with_evars & occur_meta new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
- let new_hyp_prf = clenv_value_cast_meta clenv in
+ let new_hyp_prf = clenv_value clenv in
tclTHEN
(tclEVARS (evars_of clenv.evd))
(cut_replacing id new_hyp_typ
@@ -960,8 +959,7 @@ let specialize mopt (c,lbind) g =
else
let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
let clause = clenv_unify_meta_types clause in
- let clause = clenv_expand_metas clause in
- let (thd,tstack) = whd_stack (clenv_direct_value clause) in
+ let (thd,tstack) = whd_stack (clenv_value clause) in
let nargs = List.length tstack in
let tstack = match mopt with
| Some m ->
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index dbb0d7e4f..319ed6880 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -224,11 +224,18 @@ intros x H; eapply trans_equal;
[apply H | unfold x;match goal with |- ?x = ?x => reflexivity end].
Qed.
- (* This does not work (oct 2008) because "match goal" sees "?evar = O"
- and not "O = O"
+(* Test non-regression of (temporary) bug 1981 *)
-Lemma eapply_evar : O=O -> 0=O.
-intro H; eapply trans_equal;
- [apply H | match goal with |- ?x = ?x => reflexivity end].
+Goal exists n : nat, True.
+eapply ex_intro.
+exact O.
+trivial.
+Qed.
+
+(* Test non-regression of (temporary) bug 1980 *)
+
+Goal True.
+try eapply ex_intro.
+trivial.
Qed.
-*)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 06:00:58 +0000