- else
- assert false
-(*
- begin
- prerr_endline "***************************************negative";
- let metaproof =
- incr maxmeta;
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
-(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(* print_newline (); *)
- C.Meta (!maxmeta, irl)
- in
- let eq_found =
- let proof'_old' =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Equality.ProofSymBlock (termlist, proof'_old)
- in
- let proof'_new' = assert false (* not implemented *) in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- pos,
- Equality.mk_equality
- (0, (proof'_new',proof'_old'),
- (ty, other, what, Utils.Incomparable),menv')
- in
- let target_proof =
- let pb =
- Equality.ProofBlock
- (subst, eq_URI, (name, ty), bo',
- eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
- in
- assert false, (* not implemented *)
- (match snd proof with
- | Equality.BasicProof _ ->
- (* print_endline "replacing a BasicProof"; *)
- pb
- | Equality.ProofGoalBlock (_, parent_proof) ->
- (* print_endline "replacing another ProofGoalBlock"; *)
- Equality.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false)
- in
- let refl =
- C.Appl [C.MutConstruct (* reflexivity *)
- (LibraryObjects.eq_URI (), 0, 1, []);
- eq_ty; if is_left then right else left]
- in
- (bo,
- (assert false, (* not implemented *)
- Equality.ProofGoalBlock
- (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
- end
-*)